Termination w.r.t. Q proof of /tmp/tmpn8xp8b/filliatre3.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDC(t, s(n)) → FOLDC(t, n)
F(t, x) → G(x)
FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLD(t, x, s(n)) → F(fold(t, x, n), x)
FOLDC(t, s(n)) → F(foldC(t, n), C)
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
FOLDB(t, s(n)) → FOLDB(t, n)
FOLD(t, x, s(n)) → FOLD(t, x, n)
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)

The TRS R consists of the following rules:

g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDC(t, s(n)) → FOLDC(t, n)
F(t, x) → G(x)
FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLD(t, x, s(n)) → F(fold(t, x, n), x)
FOLDC(t, s(n)) → F(foldC(t, n), C)
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
FOLDB(t, s(n)) → FOLDB(t, n)
FOLD(t, x, s(n)) → FOLD(t, x, n)
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)

The TRS R consists of the following rules:

g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 2 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDC(t, s(n)) → FOLDC(t, n)
FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLDC(t, s(n)) → F(foldC(t, n), C)
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
FOLDB(t, s(n)) → FOLDB(t, n)
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)

The TRS R consists of the following rules:

g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ RuleRemovalProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FOLDC(t, s(n)) → FOLDC(t, n)
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLDC(t, s(n)) → F(foldC(t, n), C)
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
FOLDB(t, s(n)) → FOLDB(t, n)
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)

The TRS R consists of the following rules:

foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f(t, x) → f'(t, g(x))
foldC(t, s(n)) → f(foldC(t, n), C)
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
foldC(t, 0) → t
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
f'(triple(a, b, c), C) → triple(a, b, s(c))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

FOLDC(t, s(n)) → FOLDC(t, n)
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDB(t, s(n)) → FOLDB(t, n)

Strictly oriented rules of the TRS R:

foldB(t, s(n)) → f(foldB(t, n), B)

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(A) = 1
POL(B) = 1
POL(C) = 1
POL(F(x₁, x₂)) = x₁ + 2·x₂
POL(F'(x₁, x₂)) = x₁ + 2·x₂
POL(F''(x₁)) = 1 + x₁
POL(FOLDB(x₁, x₂)) = x₁ + 2·x₂
POL(FOLDC(x₁, x₂)) = 1 + x₁ + x₂
POL(f(x₁, x₂)) = x₁ + x₂
POL(f'(x₁, x₂)) = x₁ + x₂
POL(f''(x₁)) = x₁
POL(foldB(x₁, x₂)) = x₁ + 2·x₂
POL(foldC(x₁, x₂)) = x₁ + x₂
POL(g(x₁)) = x₁
POL(s(x₁)) = 1 + x₁
POL(triple(x₁, x₂, x₃)) = 2 + x₁ + 2·x₂ + x₃

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ RuleRemovalProof

                  ↳ QDP

                    ↳ DependencyGraphProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLDC(t, s(n)) → F(foldC(t, n), C)
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)

The TRS R consists of the following rules:

foldB(t, 0) → t
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f(t, x) → f'(t, g(x))
foldC(t, s(n)) → f(foldC(t, n), C)
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
foldC(t, 0) → t
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
f'(triple(a, b, c), C) → triple(a, b, s(c))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ RuleRemovalProof

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ RuleRemovalProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FOLDC(t, s(n)) → F(foldC(t, n), C)
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)

The TRS R consists of the following rules:

foldB(t, 0) → t
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f(t, x) → f'(t, g(x))
foldC(t, s(n)) → f(foldC(t, n), C)
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
foldC(t, 0) → t
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
f'(triple(a, b, c), C) → triple(a, b, s(c))

F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))

Strictly oriented rules of the TRS R:

f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(A) = 2
POL(B) = 2
POL(C) = 2
POL(F(x₁, x₂)) = x₁ + x₂
POL(F'(x₁, x₂)) = x₁ + x₂
POL(F''(x₁)) = x₁
POL(FOLDC(x₁, x₂)) = x₁ + 2·x₂
POL(f(x₁, x₂)) = x₁ + x₂
POL(f'(x₁, x₂)) = x₁ + x₂
POL(f''(x₁)) = x₁
POL(foldB(x₁, x₂)) = x₁ + x₂
POL(foldC(x₁, x₂)) = x₁ + 2·x₂
POL(g(x₁)) = x₁
POL(s(x₁)) = 1 + x₁
POL(triple(x₁, x₂, x₃)) = x₁ + 2·x₂ + 2·x₃

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ RuleRemovalProof

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ RuleRemovalProof

                          ↳ QDP

                            ↳ DependencyGraphProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FOLDC(t, s(n)) → F(foldC(t, n), C)
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)

The TRS R consists of the following rules:

foldB(t, 0) → t
f(t, x) → f'(t, g(x))
foldC(t, s(n)) → f(foldC(t, n), C)
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
foldC(t, 0) → t
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
f'(triple(a, b, c), C) → triple(a, b, s(c))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ RuleRemovalProof

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ RuleRemovalProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))

The TRS R consists of the following rules:

foldB(t, 0) → t
f(t, x) → f'(t, g(x))
foldC(t, s(n)) → f(foldC(t, n), C)
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
foldC(t, 0) → t
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
f'(triple(a, b, c), C) → triple(a, b, s(c))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ RuleRemovalProof

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ RuleRemovalProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ RuleRemovalProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

F(t, x) → F'(t, g(x))
F'(triple(a, b, c), B) → F(triple(a, b, c), A)

The TRS R consists of the following rules:

g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C

F(t, x) → F'(t, g(x))
F'(triple(a, b, c), B) → F(triple(a, b, c), A)

Strictly oriented rules of the TRS R:

g(B) → A
g(C) → A

Used ordering: POLO with Polynomial interpretation [25]:

POL(A) = 0
POL(B) = 2
POL(C) = 2
POL(F(x₁, x₂)) = 1 + 2·x₁ + 2·x₂
POL(F'(x₁, x₂)) = 2·x₁ + 2·x₂
POL(g(x₁)) = x₁
POL(triple(x₁, x₂, x₃)) = 2 + x₁ + 2·x₂ + x₃

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ RuleRemovalProof

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ RuleRemovalProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ RuleRemovalProof

                                      ↳ QDP

                                        ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

g(A) → A
g(B) → B
g(C) → B
g(C) → C

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

FOLD(t, x, s(n)) → FOLD(t, x, n)

The TRS R consists of the following rules:

g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

FOLD(t, x, s(n)) → FOLD(t, x, n)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

FOLD(t, x, s(n)) → FOLD(t, x, n)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3